%0 Conference Proceedings
%4 dpi.inpe.br/plutao/2012/11.28.13.56.39
%2 dpi.inpe.br/plutao/2012/11.28.13.56.40
%@isbn 2012-36-0429
%F lattes: 3237709114127674 1 RomeroAmbrSouz:2012:FiStVe
%T Finite state-machine verification applied to hybrid systems
%D 2012
%A Romero, Alessandro Gerlinger,
%A Ambrosio, Ana Maria,
%A Souza, Marcelo Lopes de Oliveira e,
%@affiliation
%@affiliation Instituto Nacional de Pesquisas Espaciais (INPE)
%@affiliation Instituto Nacional de Pesquisas Espaciais (INPE)
%@electronicmailaddress romgerale@yahoo.com.br
%@electronicmailaddress ana@dss.inpe.br
%B Congresso SAE Brasil, 21.
%C São Paulo
%8 2012
%I SAE
%S Proceedings
%K state-machine, hybrid systems, source lines of code.
%X The notion of a hybrid system is centered around a composition of discrete and continuous dynamics. In particular, the system has a continuous evolution and occasional jumps. The jumps correspond to the change of state in an automaton whose transitions are caused either by controllable or uncontrollable external events or by the continuous evolution. The continuous evolution and these jumps in control loops are the origins from the most stringent temporal demands. These temporal demands are one of the reasons that hybrid systems usually require a high level of safety. Inevitably this type of system is present in mobility devices such as cars, ships and aircraft. Works present data showing that SLOC (Source Lines Of Code), one controversial metric of complexity, growth at current rate using existing development practices will seriously impact affordability of the next generation of commercial aircraft (remarkable hybrid systems). Efforts to develop this type of system have increasingly suffered from cost and schedule overruns. These trends are largely attributed to: (a) increasing system complexity, driven by requirements for increased functionality, performance and dependability; (b) using inadequate development practices. In fact, the verification of such systems has become a key activity in the development life-cycle. Historically such activity demands experts and high efforts, and uses ad-hoc methods. Therefore, the aim of this work is to apply the vast theory of automatic test case generation for this type of system, showing an effective and reproducible alternative for automatic test case generation based on finite state-machines. A case study that was developed considering the problem of inverted pendulum evaluates the suggested approach. The inverted pendulum is a model of attitude control for satellite launch vehicles at its departure (the objective of the attitude control problem is to keep the vehicle in a vertical position). The uniqueness of an inverted pendulum, due to its natural instability, provides various researches in areas of control, electronics and software. Furthermore, the inverted pendulum is a classic hybrid system, since it is composed of continuous dynamic (stabilization of the pendulum in a vertical axis) and discrete (failure mode management). This case study has given strong indications that the approach can bring significant gains for the effectiveness coupled with the reduction of time for planning and execution of verification, as well as contributing to fulfill certification requirements.
%@language en
%3 romero_finite.pdf